module Data.ForeignNat where

open import Relation.Binary.Core
open import Relation.Nullary
open import Data.Nat
open import Relation.Binary.PropositionalEquality
open import Data.Function

{-# IMPORT Data.ForeignNat.Impl #-}

data ℕ′ : Set where
  zero : ℕ′
  suc  : ℕ′ → ℕ′

pred′ : ℕ′ → ℕ′
pred′ zero    = zero
pred′ (suc n) = n
  
_≟′_ : Decidable {ℕ′}_≡_
zero  ≟′ zero   = yes refl
zero  ≟′ suc m  = no (λ ())
suc n ≟′ zero   = no (λ ())
suc n ≟′ suc m   with n ≟′ m
suc n ≟′  suc .n | yes refl = yes refl
...              | no  n≢m  = no (n≢m ∘ cong pred′)
-- ...              | no  n≢m  = no n+1≢m+1
--                        where n+1≢m+1 : (suc n) ≢ (suc m)
--                              n+1≢m+1 refl = {!!}

{-# COMPILED_DATA ℕ′ Data.ForeignNat.Impl.Nat Data.ForeignNat.Impl.Zero Data.ForeignNat.Impl.Suc #-}

marshalℕ : ℕ → ℕ′
marshalℕ  zero     = zero
marshalℕ  (suc n)  = suc (marshalℕ n)

unmarshalℕ : ℕ′ → ℕ
unmarshalℕ  zero     = zero
unmarshalℕ  (suc n)  = suc (unmarshalℕ n)

marshalℕ-id : (n : ℕ′) → (marshalℕ (unmarshalℕ n)) ≡ n
marshalℕ-id zero    = refl
marshalℕ-id (suc n) = cong suc (marshalℕ-id n)

unmarshalℕ-id : (n : ℕ) → (unmarshalℕ (marshalℕ n)) ≡ n
unmarshalℕ-id zero    = refl
unmarshalℕ-id (suc n) = cong suc (unmarshalℕ-id n)