basic support for lit naturals

Author: flupe

README.md

@@ -9,7 +9,15 @@ The backend builds off Agda 2.7.0.1.
 
 ## Setup
 
-Compatible with Coq 8.20.0 and MetaCoq 1.3.2.
+Compatible with Coq 8.19.0, MetaCoq 1.3.1 and CertiCoq 0.9.
+
+```
+opam pin add coq 8.19.0
+opam pin add certicoq 0.9+8.19
+coq_makefile -f _CoqProject -o CoqMakefile
+make -f CoqMakefile
+cabal run agda2lambox -- --out-dir build -itest test/Nat.agda
+```
 
 ## TODO
 

src/Agda2Lambox/Convert/Term.hs

@@ -13,6 +13,8 @@ import Agda.Utils
 import Agda.Syntax.Literal
 import Agda.Syntax.Abstract.Name ( QName(..), ModuleName(..) )
 import Agda.Syntax.Common.Pretty ( prettyShow )
+import Agda.TypeChecking.Primitive.Base ( getBuiltinName )
+import Agda.Compiler.Backend ( builtinNat, builtinZero, builtinSuc )
 
 import LambdaBox
 import qualified LambdaBox as L
@@ -50,7 +52,7 @@ instance A.TTerm ~> L.Term where
         A.Erased _    -> fail "Erased matches are not supported."
         A.NotErased _ -> do
           calts <- traverse go talts
-          cind <- go caseType
+          cind  <- go caseType
           return $ LCase cind 0 (LRel n) calts
     A.TUnit -> return LBox
     A.TSort -> return LBox
@@ -68,12 +70,25 @@ instance A.CaseType ~> L.Inductive where
   go = \case
     A.CTData qn -> return $ L.Inductive (qnameToKerName qn) 0 
                    -- TODO(flupe): handle mutual inductive
+
+    -- Builtin Nat
+    A.CTNat -> do
+      liftTCM (getBuiltinName builtinNat) >>= \case
+        Nothing -> fail "Builtin Nat not bound."
+        Just qn -> return $ L.Inductive (qnameToKerName qn) 0
+
     _           -> fail "Not supported case type"
 
 -- TODO(flupe): handle using MetaCoq tPrim and prim_val
 instance A.Literal ~> L.Term where
   go = \case
-    LitNat    n -> fail "Literal natural numbers not supported"
+    LitNat n -> do
+      Just qnat  <- liftTCM $ getBuiltinName builtinNat
+
+      let indnat = L.Inductive (qnameToKerName qnat) 0
+
+      return $ (!! fromInteger n) $ iterate (LApp (LCtor indnat 1 [])) (LCtor indnat 0 [])
+
     LitWord64 w -> fail "Literal int64 not supported"
     LitFloat  f -> fail "Literal float not supported"
     LitString s -> fail "Literal string not supported"

test/Nat.agda

@@ -0,0 +1,16 @@
+data Nat : Set where
+  zero : Nat
+  succ : Nat → Nat
+{-# BUILTIN NATURAL Nat #-}
+
+add : Nat → Nat → Nat
+add zero y = y
+add (succ x) y = succ (add x y)
+
+prog : Nat
+prog = add 3 2
+{-# COMPILE AGDA2LAMBOX prog #-}
+
+-- 5
+res : Nat
+res = 5