add support for nat literals

Author: flupe

agda2lambox.cabal

@@ -28,13 +28,14 @@ executable agda2lambox
                        Paths_agda2lambox
   autogen-modules:     Paths_agda2lambox
   build-depends:       base       >= 4.10  && < 4.22,
-                       Agda       >= 2.7   && <= 2.9,
+                       Agda       >= 2.8   && < 2.9,
                        deepseq    >= 1.4.4 && < 1.6,
                        queues     >= 1.0.0 && < 1.2,
                        pretty-show,
                        containers,
                        directory,
                        filepath,
+                       text,
                        mtl
   default-language:    Haskell2010
   default-extensions:

cabal.project

@@ -1,4 +1,4 @@
-packages: .
+packages: agda2lambox.cabal
 
 source-repository-package
   type: git

src/Agda2Lambox/Compile/Function.hs

@@ -19,7 +19,7 @@ import Agda.Syntax.Common ( hasQuantityω )
 import Agda.Utils.Monad (guardWithError, whenM)
 import Agda.Utils.Lens ( (^.) )
 
-import Agda.Utils ( etaExpandCtor )
+import Agda.Utils ( etaExpandCtor, treeless, pp )
 import Agda2Lambox.Compile.Utils
 import Agda2Lambox.Compile.Monad
 import Agda2Lambox.Compile.Term ( compileTerm )
@@ -35,7 +35,7 @@ isFunction _ = False
 -- | Convert a function body to a Lambdabox term.
 compileFunctionBody :: [QName] -> Definition -> CompileM LBox.Term
 compileFunctionBody ms Defn{defName, theDef} = do
-  Just t <- liftTCM $ toTreeless EagerEvaluation defName
+  Just t <- liftTCM $ treeless defName
   compileTerm ms =<< liftTCM (etaExpandCtor t)
 
 

src/Agda2Lambox/Compile/Term.hs

@@ -8,18 +8,21 @@ import Control.Monad.IO.Class (MonadIO)
 import Control.Monad.Reader.Class ( MonadReader, ask )
 import Control.Monad.Reader ( ReaderT(runReaderT), local )
 import Control.Monad.Trans
-import Data.List ( elemIndex, foldl' )
+import Data.List ( elemIndex, foldl', singleton )
 import Data.Maybe ( fromMaybe, listToMaybe )
+import Data.Foldable ( foldrM )
 
 import Agda.Compiler.Backend ( MonadTCState, HasOptions )
 import Agda.Compiler.Backend ( getConstInfo, theDef, pattern Datatype, dataMutual )
 import Agda.Syntax.Abstract.Name ( ModuleName(..), QName(..) )
+import Agda.Syntax.Builtin ( builtinZero, builtinSuc )
 import Agda.Syntax.Common ( Erased(..) )
 import Agda.Syntax.Common.Pretty ( prettyShow )
 import Agda.Syntax.Literal
 import Agda.Syntax.Treeless ( TTerm(..), TAlt(..), CaseInfo(..), CaseType(..) )
 import Agda.TypeChecking.Datatypes ( getConstructorData, getConstructors )
 import Agda.TypeChecking.Monad.Base ( TCM , liftTCM, MonadTCEnv, MonadTCM )
+import Agda.TypeChecking.Monad.Builtin ( getBuiltinName_ )
 
 import LambdaBox ( Term(..) )
 import LambdaBox qualified as LBox
@@ -125,7 +128,15 @@ compileTermC = \case
 
 compileLit :: Literal -> C LBox.Term
 compileLit = \case
-  l        -> fail $ "unsupported literal: " <> prettyShow l
+
+  LitNat i -> do
+    qz <- liftTCM $ getBuiltinName_ builtinZero
+    qs <- liftTCM $ getBuiltinName_ builtinSuc
+    z  <- liftTCM $ toConApp qz []
+    let ss = take (fromInteger i) $ repeat (toConApp qs . singleton)
+    liftTCM $ foldrM ($) z ss
+
+  l -> fail $ "unsupported literal: " <> prettyShow l
 
 compileCaseType :: CaseType -> C LBox.Inductive
 compileCaseType = \case

src/Main.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE DeriveGeneric, DeriveAnyClass, NamedFieldPuns #-}
+{-# LANGUAGE DeriveGeneric, DeriveAnyClass, NamedFieldPuns, OverloadedStrings #-}
 -- | The agda2lambox Agda backend
 module Main (main) where
 
@@ -9,6 +9,7 @@ import Data.Function ( (&) )
 import Data.IORef ( IORef, newIORef, readIORef, modifyIORef' )
 import Data.Maybe ( fromMaybe, catMaybes )
 import Data.Version ( showVersion )
+import Data.Text ( pack )
 import GHC.Generics ( Generic )
 import System.Console.GetOpt ( OptDescr(Option), ArgDescr(ReqArg) )
 import System.Directory ( createDirectoryIfMissing )
@@ -57,7 +58,9 @@ agda2lambox = Backend backend
     backend :: Backend' Options Options ModuleEnv ModuleRes QName
     backend = Backend'
       { backendName           = "agda2lambox"
-      , backendVersion        = Just $ showVersion version
+      , backendInteractTop    = Nothing
+      , backendInteractHole   = Nothing
+      , backendVersion        = Just $ pack $ showVersion version
       , options               = defaultOptions
       , commandLineFlags      =
           [ Option ['o'] ["out-dir"] (ReqArg outdirOpt "DIR")

test/Imports.agda

@@ -1,5 +1,13 @@
 open import Agda.Builtin.Bool
 open import Agda.Builtin.List
+open import Agda.Builtin.Nat
 
 test : List Bool
 test = true ∷ false ∷ []
+
+map : {A B : Set} → (A → B) → List A → List B
+map f [] = []
+map f (x ∷ xs) = f x ∷ map f xs
+
+test2 : List Nat
+test2 = map suc (1 ∷ [])