Add special rules for Nat zero and suc constructors

Author: jespercockx

src/Agda2Hs/Compile/Name.hs

@@ -65,6 +65,8 @@ toNameImport x (Just mod) =
 defaultSpecialRules :: SpecialRules
 defaultSpecialRules = Map.fromList
   [ "Agda.Builtin.Nat.Nat"          `to` "Natural"      `importing` Just "Numeric.Natural"
+  , "Agda.Builtin.Nat.Nat.zero"     `to` "0"            `importing` Nothing
+  , "Agda.Builtin.Nat.Nat.suc"      `to` "succ"         `importing` Nothing
   , "Haskell.Prelude.coerce"        `to` "unsafeCoerce" `importing` Just "Unsafe.Coerce"
   , "Agda.Builtin.Int.Int"          `to` "Integer"      `importing` Nothing
   , "Agda.Builtin.Word.Word64"      `to` "Word"         `importing` Nothing

test/Succeed/ZeroSuc.agda

@@ -0,0 +1,26 @@
+module ZeroSuc where
+
+open import Haskell.Prelude
+
+test1 : Nat
+test1 = zero
+
+{-# COMPILE AGDA2HS test1 #-}
+
+test2 : Nat → Nat
+test2 = suc
+
+{-# COMPILE AGDA2HS test2 #-}
+
+data MyNat : Set where
+  MyZero : MyNat
+  MySuc : MyNat → MyNat
+
+{-# COMPILE AGDA2HS MyNat #-}
+
+opaque
+  test3 : MyNat → Nat
+  test3 MyZero = zero
+  test3 (MySuc n) = suc (test3 n)
+
+{-# COMPILE AGDA2HS test3 #-}

test/Succeed/ZeroSuc.hs

@@ -0,0 +1,17 @@
+module ZeroSuc where
+
+import Numeric.Natural (Natural)
+
+test1 :: Natural
+test1 = 0
+
+test2 :: Natural -> Natural
+test2 = succ
+
+data MyNat = MyZero
+           | MySuc MyNat
+
+test3 :: MyNat -> Natural
+test3 MyZero = 0
+test3 (MySuc n) = succ (test3 n)
+