[ fix #385 ] Implement predNat primitive

CHANGELOG.md

@@ -9,6 +9,12 @@ See https://github.com/agda/agda2hs/issues?q=milestone%3A1.5+is%3Apr for the ful
 Additions to the agda2hs Prelude
 --------------------------------
 
+- Added `predNat` to `Haskell.Extra.Nat`: the predecessor of a nonzero
+  natural number, returning the predecessor together with a proof that
+  the original number is its successor. It compiles to Haskell's `pred`
+  and enables defining functions such as a `Nat` recursor on top of
+  `ifDec` (see issue #385).
+
 
 Fixed issues
 ------------

lib/base/Haskell/Extra/Nat.agda

@@ -0,0 +1,11 @@
+module Haskell.Extra.Nat where
+
+open import Haskell.Prelude
+open import Haskell.Extra.Refinement
+
+-- | The predecessor of a nonzero natural number, together with a proof
+-- that the original number is its successor. Since pattern matching on
+-- 'Nat' is not allowed in Haskell, this is provided as a primitive that
+-- compiles to Haskell's 'pred'.
+postulate
+  predNat : (n : Nat) → @0 (n ≡ 0 → ⊥) → ∃ Nat λ m → n ≡ suc m

src/Agda2Hs/Compile/Term.hs

@@ -66,6 +66,7 @@ isSpecialDef q = case prettyShow q of
   "Haskell.Prim.the"             -> Just expTypeSig
   "Haskell.Extra.Delay.runDelay" -> Just compileErasedApp
   "Agda.Builtin.Word.primWord64FromNat" -> Just primWord64FromNat
+  "Haskell.Extra.Nat.predNat"            -> Just predNat
   _                              -> Nothing
 
 
@@ -137,6 +138,14 @@ primWord64FromNat ty args = compileArgs ty args >>= \case
   -- anything else
   _ -> agda2hsError "primWord64FromNat must be applied to a literal"
 
+-- | Compile 'predNat' to Haskell's 'pred'. The erased proof argument is
+-- dropped by 'compileArgs', so the single remaining argument is the
+-- natural number whose predecessor we want.
+predNat :: DefCompileRule
+predNat ty args = compileArgs ty args >>= \case
+  n : es' -> return $ eApp (hsVar "pred") [n] `eApp` es'
+  _       -> agda2hsError "predNat must be applied to a natural number"
+
 
 compileVar :: Int -> Type -> [Term] -> C (Hs.Exp ())
 compileVar i ty es = do

test/Succeed/PredNat.agda

@@ -0,0 +1,27 @@
+module PredNat where
+
+open import Haskell.Prelude
+open import Haskell.Extra.Dec
+open import Haskell.Extra.Nat
+open import Haskell.Extra.Refinement
+open import Haskell.Law.Eq
+open import Haskell.Law.Eq.Instances
+
+-- The predecessor of a nonzero natural number.
+predNat' : (n : Nat) → @0 (n ≡ 0 → ⊥) → Nat
+predNat' n neq = predNat n neq .value
+
+{-# COMPILE AGDA2HS predNat' #-}
+
+-- A recursor for natural numbers, as suggested in issue #385.
+recNat : (a : @0 Nat → Set)
+       → (z : a 0)
+       → (s : (m : Nat) → a m → a (suc m))
+       → (n : Nat) → a n
+recNat a z s n = ifDec (n ≟ 0)
+  (λ where {{refl}} → z)
+  (λ {{n≠0}} →
+    case predNat n n≠0 of λ where
+      (m ⟨ refl ⟩) → s m (recNat a z s m))
+
+{-# COMPILE AGDA2HS recNat #-}

test/Succeed/PredNat.hs

@@ -0,0 +1,13 @@
+module PredNat where
+
+import Numeric.Natural (Natural)
+
+predNat' :: Natural -> Natural
+predNat' n = pred n
+
+recNat :: a -> (Natural -> a -> a) -> Natural -> a
+recNat z s n
+  = if n == 0 then z else
+      case pred n of
+          m -> s m (recNat z s m)
+